Nuprl Lemma : chain_master_ind_wf
11,40
postcript
pdf
X
:Type,
x
:chain_master(),
config
:((Id List)
X
),
seq
:(Id
Id
X
).
case
x
of config(
list
) =>
config
(
list
) seq(
from
,
to
,
num
) =>
seq
(
from
,
to
,
num
)
X
latex
Definitions
t
.2
,
t
.1
,
x
(
s1
,
s2
,
s3
)
,
x
(
s
)
,
case
x
of config(
list
) =>
config
(
list
) seq(
from
,
to
,
num
) =>
seq
(
from
;
to
;
num
)
,
t
T
,
x
:
A
.
B
(
x
)
,
chain_master()
Lemmas
chain
master
wf
,
nat
wf
,
Id
wf
origin
X:Type, x:chain_master(), config:((Id List)
X), seq:(IdId
X).
X X:Type, x:chain_master(), config:((Id List)X), seq:(IdIdX).
X Tx:A. B(x)